{-
 This file is part of the Clafer to Alloy Translator (clafer2alloy).

 Copyright (C) 2010 Kacper Bak <http://gsd.uwaterloo.ca/kbak>

 clafer2alloy is free software: you can redistribute it and/or modify
 it under the terms of the GNU Lesser General Public License as published by
 the Free Software Foundation, either version 3 of the License, or
 (at your option) any later version.

 clafer2alloy is distributed in the hope that it will be useful,
 but WITHOUT ANY WARRANTY; without even the implied warranty of
 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 GNU Lesser General Public License for more details.

 You should have received a copy of the GNU Lesser General Public License
 along with clafer2alloy. (See files COPYING and COPYING.LESSER.)  If not,
 see <http://www.gnu.org/licenses/>.
-}
module StringAnalyzer where

import Absclafer2alloy
import Data.Map (Map)
import qualified Data.Map as Map
import Control.Monad.State

-- -----------------------------------------------------------------------------
type StringTable = Map String Int

astrModule :: Module -> Module
astrModule x = case x of
  Module declarations ->
    Module $ evalState (mapM astrDeclaration declarations) $ Map.empty


astrDeclaration x = case x of
  EnumDecl ident enumids  -> error "desugared"
  AbsClaferDecl gcard ident super attr elements  ->
    AbsClaferDecl gcard ident super attr `liftM` astrElements elements
  ClaferDecl clafer  -> ClaferDecl `liftM` astrClafer clafer
  ConstDecl constraint  -> ConstDecl `liftM` astrConstraint constraint


-- astrs non-abstract clafer
astrClafer x = case x of
  Clafer gcard ident super attr essential card elements  ->
    Clafer gcard ident super attr essential card `liftM` astrElements elements


-- astrs subclafers
astrElements x = case x of
  ElementsEmpty  -> error "desugred"
  Elements elements  -> do Elements `liftM` mapM astrElement elements


-- astrs single subclafer
astrElement x = case x of
  Subclafer clafer  -> Subclafer `liftM` astrClafer clafer
  ClaferUse name essential card elements -> error "desugared"
  Subconstraint constraint  -> Subconstraint `liftM` astrConstraint constraint


astrConstraint x = case x of
  Constraint essential lexps -> Constraint essential `liftM` mapM astrLExp lexps


astrLExp x = case x of
  EIff lexp0 iff lexp  -> ale EIff iff [lexp0, lexp]
  EImplies lexp0 implies lexp  -> ale EImplies implies [lexp0, lexp]
  EImpliesElse lexp0 implies lexp1 lexp  ->
    applyExps (apply3 EImpliesElse implies) astrLExp [lexp0, lexp1, lexp]
  EOr lexp0 or lexp  -> ale EOr or [lexp0, lexp]
  EXor lexp0 xor lexp  -> ale EXor xor [lexp0, lexp]
  EAnd lexp0 and lexp  -> ale EAnd and [lexp0, lexp]
  ENeg neg lexp  -> ENeg neg `liftM` astrLExp lexp
  ETerm term  -> ETerm `liftM` astrTerm term
  where
  ale cons op ls = applyExps (apply2 cons op) astrLExp ls
  apply2 cons op (x1:x2:[])    = cons x1 op x2
  apply3 cons op (x1:x2:x3:[]) = cons x1 op x2 x3


applyExps f mf ls = f `liftM` mapM mf ls


astrTerm x = case x of
  TermCmpExp cmpexp  -> TermCmpExp `liftM` astrCmpExp cmpexp
  TermQuantDeclExp decls lexp -> TermQuantDeclExp decls `liftM` astrLExp lexp
  _ -> return x


astrCmpExp x = case x of
  ELt exp0 exp  -> ae ELt [exp0, exp]
  EGt exp0 exp  -> ae EGt [exp0, exp]
  EREq exp0 exp -> ae EREq [exp0, exp]
  EEq exp0 exp  -> ae EEq [exp0, exp]
  ELte exp0 exp  -> ae ELte [exp0, exp]
  EGte exp0 exp  -> ae EGte [exp0, exp]
  ENeq exp0 exp  -> ae ENeq [exp0, exp]
  ERNeq exp0 exp -> ae ERNeq [exp0, exp]
  EIn exp0 exp   -> ae EIn  [exp0, exp]
  ENin exp0 exp  -> ae ENin [exp0, exp]
  where
  ae cons ls = applyExps (apply2 cons) astrExp ls
  apply2 cons (x1:x2:[]) = cons x1 x2


astrExp x = case x of
  EStrExp (EStr string) -> do
    modify (\e -> Map.insertWith const string (Map.size e) e)
    st <- get
    return $ ENumExp $ EInt $ toInteger $ (Map.!) st string
  _ -> return x
